Step of Proof: squash_thru_equiv_rel
12,41
postcript
pdf
Inference at
*
3
I
of proof for Lemma
squash
thru
equiv
rel
:
1.
T
: Type
2.
E
:
T
T
3.
((
a
:
T
.
E
(
a
,
a
)) & (
a
,
b
:
T
.
E
(
a
,
b
)
E
(
b
,
a
)) & (
a
,
b
,
c
:
T
.
E
(
a
,
b
)
E
(
b
,
c
)
E
(
a
,
c
)))
4.
a
:
T
5.
b
:
T
6.
c
:
T
7.
E
(
a
,
b
)
8.
E
(
b
,
c
)
E
(
a
,
c
)
latex
by OnClauses [3;7;8;0] D
latex
1
:
1:
3. (
a
:
T
.
E
(
a
,
a
)) & (
a
,
b
:
T
.
E
(
a
,
b
)
E
(
b
,
a
)) & (
a
,
b
,
c
:
T
.
E
(
a
,
b
)
E
(
b
,
c
)
E
(
a
,
c
))
1:
4.
a
:
T
1:
5.
b
:
T
1:
6.
c
:
T
1:
7.
E
(
a
,
b
)
1:
8.
E
(
b
,
c
)
1:
E
(
a
,
c
)
.
Definitions
t
T
,
True
,
T
origin